Merge pull request #10 from plclub/yesclose

Put back generating close definitions

.github/workflows/build.yml

@@ -16,6 +16,7 @@ jobs:
       matrix:
         resolver:
           - nightly
+          - lts-22
           - lts-21
           - lts-20
           - lts-19

README.md

@@ -25,11 +25,7 @@ Dependencies
   Recently tested with GHC 8.10.7
 
 * LNgen's output must be combined with the output of
-  [Ott](https://github.com/ott-lang/ott).  
-
-  Obtain Ott from https://github.com/sweirich/ott 
-
-  (Fork of ott.0.31)
+  [Ott](https://github.com/ott-lang/ott). Obtain Ott from opam.
 
 * The Coq Proof assistant.
 
@@ -108,6 +104,10 @@ The following options to `lngen` may be useful:
   option can  be used  to `Require` the  library generated by  Ott.  (In
   fact, LNgen's output won't compile without it.)
 
+* --coq-nolcset : Suppress the Set version of local closure
+
+* --coq-noclose : Suppress generation of `close` and `close_rec` definitions
+
 
 Restrictions on Ott specifications
 ==================================

app/Main.hs

@@ -48,6 +48,7 @@ options =
     , Option []    ["coq-ott"]       (ReqArg CoqOtt "LIB")      "Coq: name of library to Require"
     , Option []    ["coq-stdout"]    (NoArg CoqStdout)          "Coq: send output to standard out"
     , Option []    ["coq-nolcset"]   (NoArg CoqNoLCSet)         "Coq: suppress the Set version of local closure"
+    , Option []    ["coq-noclose"]   (NoArg CoqNoClose)         "Coq: suppress generation of close and close_rec"
     , Option ['?'] ["help"]          (NoArg Help)               "displays usage information"
     ]
 

src/ComputationMonad.hs

@@ -30,7 +30,8 @@ data ProgFlag
     | CoqOtt String      -- ^ Name of the library to @Require@ in generated output.
     | CoqOutput String   -- ^ Destination for output.
     | CoqStdout          -- ^ Send output to standard out.
-    | CoqNoLCSet         -- ^ Suppress the Set version of Local Closure
+    | CoqNoLCSet         -- ^ Suppress the Set version of Local Closure.
+    | CoqNoClose         -- ^ Suppress generation of close and close_rec.
     | Help               -- ^ Display usage information.
     deriving ( Eq )
 
@@ -145,3 +146,7 @@ reset =
 {- | Check whether to not generate lc set  -}
 nolcset :: [ProgFlag] -> Bool
 nolcset = elem CoqNoLCSet
+
+{- | Check whether to not generate close  -}
+noclose :: [ProgFlag] -> Bool
+noclose = elem CoqNoClose

src/CoqLNOutput.hs

@@ -24,6 +24,7 @@ import CoqLNOutputThmSwap
 import CoqLNOutputThmSubst
 import MyLibrary ( nmap )
 import Control.Monad (filterM)
+import Control.Monad.State (get)
 
 
 {- ----------------------------------------------------------------------- -}
@@ -37,7 +38,10 @@ coqOfAST :: Maybe String -> Maybe String -> AST -> M String
 coqOfAST ott loadpath ast =
     do { nts'       <- filter (not . null) <$>
                        mapM (local . filterM (notPhantomNtRoot aa)) nts
+       ; (flags, _)   <- get
+       ; let suppress x = if noclose flags then "" else x
        ; bodyStrs   <- mapM (local . processBody aa) nts'
+       ; closeStrs  <- mapM (local . processClose aa) nts
        ; degreeStrs <- mapM (local . processDegree aa) nts'
        ; lcStrs     <- mapM (local . processLc aa) nts'
        ; ntStrs     <- mapM (local . processNt aa) nts'
@@ -76,6 +80,8 @@ coqOfAST ott loadpath ast =
                   \\n" ++
                   coqSep ++ "(** * Induction principles for nonterminals *)\n\n" ++
                   concat ntStrs ++ "\n" ++
+                  suppress (coqSep ++ "(** * Close *)\n\n" ++
+                            concat closeStrs ++ "\n") ++
                   coqSep ++ "(** * Size *)\n\n" ++
                   concat sizeStrs ++ "\n" ++
                   coqSep ++ "(** * Degree *)\n\

src/CoqLNOutputDefinitions.hs

@@ -6,6 +6,7 @@
 
 module CoqLNOutputDefinitions
     ( processBody
+    , processClose
     , processDegree
     , processLc
     , processNt
@@ -98,6 +99,124 @@ processBody aaa nt1s =
              ; return $ "#[export] Hint Unfold " ++ body ++ " : core.\n\n"
              }
 
+
+{- ----------------------------------------------------------------------- -}
+{- * Output for @close@ -}
+
+{- | Generates the text for the @close@ and @close_rec@ functions. -}
+
+processClose :: ASTAnalysis -> [NtRoot] -> M String
+processClose aa nts =
+    do { s1 <- processCloseRecs aa nts
+       ; s2 <- processCloseDefs aa nts
+       ; return $ s1 ++ s2
+       }
+
+{- | Generates the text for the definitions of @close@. -}
+
+processCloseDefs :: ASTAnalysis -> [NtRoot] -> M String
+processCloseDefs aaa nt1s =
+    do { ss <- processNt1Nt2Mv2 aaa nt1s f
+       ; return $ concat $ concat ss
+       }
+    where
+      f aa nt1 _ mv2 =
+          do { fn    <- closeName aa nt1 mv2
+             ; fnrec <- closeRecName aa nt1 mv2
+             ; e     <- newName nt1
+             ; x     <- newName mv2
+             ; return $ printf
+               "Definition %s %s %s := %s 0 %s %s.\n\n"
+               fn x e fnrec x e
+             }
+
+{- | Generates the text for the definitions of @close_rec@. -}
+
+processCloseRecs :: ASTAnalysis -> [NtRoot] -> M String
+processCloseRecs aaa nt1s =
+    do { ss <- processNt1Nt2Mv2 aaa nt1s f
+       ; return $ concat $ map join $ ss
+       }
+    where
+      join strs = printf "Fixpoint %s.\n\n" (sepStrings "\n\nwith " strs)
+
+      f aa nt1 nt2 mv2 =
+        do { close           <- closeRecName aa nt1 mv2
+           ; k               <- newName bvarRoot
+           ; x               <- newName mv2
+           ; xtype           <- mvType aa mv2
+           ; e               <- newName nt1
+           ; etype           <- ntType aa nt1
+           ; (Syntax _ _ _ cs) <- getSyntax aa nt1
+           ; branches        <- mapM (local . branch k x nt1 nt2 mv2) cs
+           ; return $ printf
+             "%s (%s : %s) (%s : %s) (%s : %s) {struct %s} : %s :=\n\
+             \  match %s with\n\
+             \%s\n\
+             \  end"
+             close k bvarType x xtype e etype e etype
+             e
+             (sepStrings "\n" branches)
+            }
+
+      branch k _ nt1 nt2 mv2 c@(SConstr _ _ _ _ (Bound mv'))
+          | canonRoot aaa nt1 == canonRoot aaa nt2 &&
+            canonRoot aaa mv2 == canonRoot aaa mv' =
+                do { n <- newName bvarRoot
+                   ; return $ printf
+                     "    | %s %s => if (%s %s %s) then (%s %s) else (%s %s)"
+                     (toName c) n
+                     bvarLtGeDec n k
+                     (toName c) n
+                     (toName c) ("(S " ++ n ++ ")")
+                   }
+
+      branch k x nt1 nt2 mv2 c@(SConstr _ _ _ _ (Free mv'))
+                | canonRoot aaa nt1 == canonRoot aaa nt2 &&
+                  canonRoot aaa mv2 == canonRoot aaa mv' =
+              do { y   <- newName mv2
+                 ; bsc <- getBoundVarConstr aaa nt1 mv2
+                 ; return $ printf
+                   "    | %s %s => if (%s == %s) then (%s %s) else (%s %s)"
+                   (toName c) y
+                   x y
+                   (toName bsc) k
+                   (toName c) y
+                 }
+      branch k x nt1 nt2 mv2 c@(SConstr _ _ _ ts _) =
+          do { args  <- mapM (newName . toRoot) ts
+             ; calls <- mapM (call k x nt1 nt2 mv2) (zip ts args)
+             ; return $ printf
+               "    | %s%s => %s%s"
+               (toName c)
+               (sepStrings " " ("" : args))
+               (toName c)
+               (sepStrings " " ("" : calls))
+             }
+
+      call _ _ _ _ _ (IndexArg, z) = return z
+      call _ _ _ _ _ (MvArg _,  z) = return z
+
+      call k x _ nt2 mv2 (NtArg nt, z)
+          | canBindIn aaa nt2 nt =
+              do { fn <- closeRecName aaa nt mv2
+                 ; return $ printf "(%s %s %s %s)" fn k x z
+                 }
+          | otherwise =
+              return z
+
+      call k x nt1 nt2 mv2 (BindingArg mv' ntm nt, z)
+          | canonRoot aaa ntm == canonRoot aaa nt2 &&
+            canonRoot aaa mv2 == canonRoot aaa mv' =
+                do { fn <- closeRecName aaa nt mv2
+                   ; return $ printf
+                     "(%s %s %s %s)"
+                     fn ("(S " ++ k ++ ")") x z
+                   }
+          | otherwise =
+              call k x nt1 nt2 mv2 (NtArg nt, z)
+
+
 {- ----------------------------------------------------------------------- -}
 {- * Output for @degree@ -}
 

stack.yaml

@@ -2,7 +2,7 @@
 
 # Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2)
 # ghc-8.10.7
-resolver: lts-19.2
+resolver: lts-22.38
 
 # Local packages, usually specified by relative directory name
 packages: