From ddef12e7957fd8cd517fbf81be4464253820af30 Mon Sep 17 00:00:00 2001 From: Takametaka Date: Fri, 12 Jun 2020 12:17:20 +0200 Subject: [PATCH 1/2] add agda system and agda checking script --- src/core/systems.ml | 11 ++- src/sttfa/export/agda.ml | 175 +++++++++++++++++++++++++++++++++++++++ src/sttfa/exporter.ml | 2 + utils/checking/agda.sh | 23 +++++ utils/export.sh | 3 +- 5 files changed, 209 insertions(+), 5 deletions(-) create mode 100644 src/sttfa/export/agda.ml create mode 100755 utils/checking/agda.sh diff --git a/src/core/systems.ml b/src/core/systems.ml index 5f1d58c..b7c1e14 100644 --- a/src/core/systems.ml +++ b/src/core/systems.ml @@ -1,6 +1,6 @@ -type t = Coq | Matita | Pvs | OpenTheory | Lean | Hollight | Latex +type t = Coq | Matita | Pvs | OpenTheory | Lean | Hollight | Latex | Agda -let systems = [Coq ; Matita ; Pvs ; OpenTheory ; Lean ; Hollight ; Latex] +let systems = [Coq ; Matita ; Pvs ; OpenTheory ; Lean ; Hollight ; Latex ; Agda] exception UnsupportedSystem of string @@ -23,7 +23,8 @@ let spec : spec list = ; ( "pvs" , Pvs ) ; ( "lean" , Lean ) ; ( "hollight" , Hollight ) - ; ( "latex" , Latex )] |> + ; ( "latex" , Latex ) + ; ( "agda" , Agda )] |> List.sort (fun (s,_) (t,_) -> String.compare s t) (** Maps system to their extension. *) @@ -34,7 +35,8 @@ let exts : (t * string) list = ; ( OpenTheory, "ot" ) ; ( Lean , "lean" ) ; ( Hollight , "ml" ) - ; ( Latex , "tex" ) ] + ; ( Latex , "tex" ) + ; ( Agda , "agda" ) ] (** [of_string str] returns the system associated to the string [str]. *) let of_string : string -> t = fun s -> @@ -49,3 +51,4 @@ let to_string : t -> string = function | Pvs -> "pvs" | Lean -> "lean" | Latex -> "latex" + | Agda -> "agda" diff --git a/src/sttfa/export/agda.ml b/src/sttfa/export/agda.ml new file mode 100644 index 0000000..089acd5 --- /dev/null +++ b/src/sttfa/export/agda.ml @@ -0,0 +1,175 @@ +module D = Core.Deps +open Ast + +let sys = "agda" + +let cur_md = ref "" + +(* no files in arith_fermat are using them but we still might get new files using them in the future *) +let forbidden_id = ref ["abstract";"consructor";"data";"do";"eta-equality";"field";"forall";"hiding"; + "import";"in";"inductive";"infix";"infixl";"infixr";"instance";"let";"macro"; + "module";"mutual";"no-eta-equality";"open";"overlap";"pattern";"postulate"; + "primitive";"private";"public";"quote";"quoteContext";"quoteGoal";"quoteTerm"; + "record";"renaming";"rexrite";"Set";"syntax";"tactic";"unquote";"unquoteDecl"; + "unquoteDef";"using";"variable";"where";"with"] + +(* when _ used as wildcard, leave it + otherwise, change it to :: (- is forbidden because it may lead to inline comments) + because i would be interpreted as mix-fix operator *) +let sanitize id = + if id = "_" + then id + else + if List.mem id !forbidden_id + then + "dk^"^id + else + let regexp = Str.regexp "_" in + Str.global_replace regexp "::" id + +let print_var oc id = + Format.fprintf oc "%s" (sanitize id) + +let rec print_list sep pp oc = function + | [] -> Format.fprintf oc "" + | [x] -> Format.fprintf oc "(%a)" pp x + | x::t -> Format.fprintf oc "(%a)%s%a" pp x sep (print_list sep pp) t + +let print_dep oc dep = + (* let dep = sanitize dep in *) + Format.fprintf oc "open import %s\n" dep + +let print_name oc (md,id) = + let id = sanitize id in + (* let md = sanitize md in *) + (* sanitize md causes problems, one might need to rename all files with : + (cd export/agda ; rename _ :: *.agda) *) + if !cur_md = md then + Format.fprintf oc "%s" id + else + Format.fprintf oc "%s.%s" md id + +let rec print_arity oc arity = + if arity = 0 then + Format.fprintf oc "Set" + else + Format.fprintf oc "Set -> %a" print_arity (arity-1) + +let rec print__ty oc = function + | TyVar(var) -> + Format.fprintf oc "%a" print_var var + | Arrow(_tyl,_tyr) -> + Format.fprintf oc "%a -> %a" print__ty_wp _tyl print__ty _tyr + | TyOp(tyOp, []) -> + Format.fprintf oc "%a" print_name tyOp + | TyOp(tyOp, _tys) -> + Format.fprintf oc "%a %a" print_name tyOp (print_list " " print__ty) _tys + | Prop -> Format.fprintf oc "Prop" + +and print__ty_wp fmt _ty = + match _ty with + | TyVar _ + | Prop + | TyOp _ -> print__ty fmt _ty + | Arrow _ -> Format.fprintf fmt "(%a)" print__ty _ty + +let rec print_ty oc = function + | ForallK(var, ty) -> + (* Format.fprintf oc "forall (%a : Set) -> %a" print_var var print_ty ty *) + Format.fprintf oc "(%a : Set) -> %a" print_var var print_ty ty + | Ty(_ty) -> print__ty oc _ty + +let rec print__te oc = function + | TeVar(var) -> + Format.fprintf oc "%a" print_var var + | Abs(var,_ty,_te) -> + Format.fprintf oc "\\(%a : %a) -> %a" print_var var print__ty_wp _ty print__te _te + | App(Abs _ as _tel,_ter) -> (* Some proofs are not in beta normal form (is it true for Agda ?) *) + Format.fprintf oc "((%a) %a)" print__te _tel print__te_wp _ter (* not sure *) + | App(_tel,_ter) -> + Format.fprintf oc "%a %a" print__te _tel print__te_wp _ter (* not sure *) + | Forall(var,_ty,_te) -> + Format.fprintf oc "(%a : %a) -> %a" print_var var print__ty_wp _ty print__te _te + (* Format.fprintf oc "forall (%a : %a) -> %a" print_var var print__ty_wp _ty print__te _te *) + | Impl(_tel,_ter) -> + Format.fprintf oc "%a -> %a" print__te_wp _tel print__te _ter + | AbsTy(var, _te) -> + Format.fprintf oc "\\(%a : Set) -> %a" print_var var print__te _te (* ie id = \(A : Set) -> \(x : A) -> x *) + | Cst(cst, []) -> + Format.fprintf oc "%a" print_name cst + | Cst(cst, _tys) -> + Format.fprintf oc "%a %a" print_name cst (print_list " " print__ty) _tys + +and print__te_wp fmt _te = + match _te with + | TeVar _ + | Cst(_,[]) -> Format.fprintf fmt "%a" print__te _te + | _ -> Format.fprintf fmt "(%a)" print__te _te + +let rec print_te oc = function + | ForallP(var,te) -> + Format.fprintf oc "(%a : _) -> %a" print_var var print_te te + (* Format.fprintf oc "forall %a -> %a" print_var var print_te te *) + | Te(_te) -> print__te oc _te + +let rec print_proof oc = function + | Assume(_,var) -> Format.fprintf oc "%a" print_var var + | Lemma(name,_) -> Format.fprintf oc "%a" print_name name + | Conv(_,proof,_) -> Format.fprintf oc "%a" print_proof proof + | ImplE(_,left,right) -> Format.fprintf oc "(%a) (%a)" print_proof left print_proof right + | ImplI(_,proof,var) -> (* abstraction to indtroduce Impl, needs to extract term from judgment *) + let j' = judgment_of proof in + let _,_te = TeSet.choose (TeSet.filter (fun (x,_) -> if x = var then true else false) j'.hyp) in + Format.fprintf oc "\\(%a : %a) -> (%a)" print_var var print__te _te print_proof proof + | ForallE(_,proof,_te) -> Format.fprintf oc "(%a) (%a)" print_proof proof print__te _te + | ForallI(_,proof,var) -> + let j' = judgment_of proof in + let _,_ty = List.find (fun (x,_) -> x = var) j'.te in + Format.fprintf oc "\\(%a : %a) -> %a" print_var var print__ty _ty print_proof proof + | ForallPE(_,proof,_ty) -> Format.fprintf oc "(%a) (%a)" print_proof proof print__ty _ty + | ForallPI(_,proof,var) -> + Format.fprintf oc "\\(%a : Set) -> %a" print_var var print_proof proof + +let print_item oc = function + | Parameter(name,ty) -> + Format.fprintf oc "%a : %a@." print_name name print_ty ty + | Definition(name,ty,te) -> + Format.fprintf oc "%a : %a@.%a = %a@.@." print_name name print_ty ty print_name name print_te te + | Axiom (name,te) -> + Format.fprintf oc "postulate %a : %a@." print_name name print_te te + | Theorem(name,te,proof) -> + Format.fprintf oc "%a : %a@.%a = %a@.@." print_name name print_te te print_name name print_proof proof + | TypeDecl(tyop,arity) -> + Format.fprintf oc "%a : %a@." print_name tyop print_arity arity + | TypeDef (name,_,_) -> + Format.fprintf oc "-- Type definition (for %a) not handled right now@." print_name name + +let print_ast : Format.formatter -> ?mdeps:Ast.mdeps -> Ast.ast -> unit = fun fmt ?mdeps:_ ast -> + cur_md := ast.md; + Format.fprintf fmt "module %s where\n" !cur_md; + D.QSet.iter (print_dep fmt) ast.dep; + List.iter (print_item fmt) ast.items + +(* not used ? +let print_meta_ast fmt meta_ast = + let print_ast fmt ast = + Format.fprintf fmt "module %s where\n" ast.md; (* I don't think you need to indent for a top-level module *) + print_ast fmt ast; + in + List.iter (print_ast fmt) meta_ast + +let to_string fmt = Format.asprintf "%a" fmt +*) + +let string_of_item = function + | Parameter((_,id),ty) -> + Format.asprintf "%s : %a" id print_ty ty + | Definition((_,id),ty,te) -> + Format.asprintf "%s : %a@.%s = %a" id print_ty ty id print_te te + | Axiom((_,id),te) -> + Format.asprintf "postulate %s : %a" id print_te te + | Theorem((_,id),te,_) -> + Format.asprintf "%s : %a" id print_te te + | TypeDecl((_,id),arity) -> + Format.asprintf "%s : %a" id print_arity arity + | TypeDef _ -> failwith "[AGDA] Type definitions not handled right now" diff --git a/src/sttfa/exporter.ml b/src/sttfa/exporter.ml index 96418a3..c6cca0b 100644 --- a/src/sttfa/exporter.ml +++ b/src/sttfa/exporter.ml @@ -15,6 +15,7 @@ let export_to_system_as_string : Systems.t -> Ast.item -> string = fun sys -> | Lean -> Lean.string_of_item | Hollight -> Hollight.string_of_item | Pvs -> Pvs.string_of_item + | Agda -> Agda.string_of_item | _ -> assert false let export_to_system_as_ast : Systems.t -> Format.formatter -> @@ -26,6 +27,7 @@ let export_to_system_as_ast : Systems.t -> Format.formatter -> | Lean -> Lean.print_ast | Hollight -> Hollight.print_ast | Pvs -> Pvs.print_ast + | Agda -> Agda.print_ast | _ -> assert false (** [mk_ast md es] creates the STTfa ast of entries [es] from dedukti module diff --git a/utils/checking/agda.sh b/utils/checking/agda.sh new file mode 100755 index 0000000..9f04e1b --- /dev/null +++ b/utils/checking/agda.sh @@ -0,0 +1,23 @@ +#!/bin/bash + +usage="Agda checker: $0 -d " + +while getopts 'hd:' arg; do + case "$arg" in + d) + indir=$OPTARG + ;; + h) + echo "$usage" + exit 0 + ;; + esac +done + +if [[ -z ${indir:-''} ]] +then + echo -e 'Directory containing source files not specified' + echo -e "$usage" + exit 1 +fi +(cd ${indir} ; find . -type f -name "*.agda" -exec agda -W noMissingDefinitions --type-in-type --prop {} \;) diff --git a/utils/export.sh b/utils/export.sh index 87f224a..a9108b6 100755 --- a/utils/export.sh +++ b/utils/export.sh @@ -46,7 +46,8 @@ middleware=${mid:-"$thy"} --pvs "export/pvs"\ --lean "export/lean"\ --coq "export/coq"\ - --matita "export/matita" + --matita "export/matita"\ + --agda "export/agda" else dune exec -- eksporti "$exp" -I "$thdir" -I "$srcdir" -o "$out"\ -d "$srcdir" -m "$middleware" From 9c3284e9bd66ea799c73cfcfb561a6070e4fb7a0 Mon Sep 17 00:00:00 2001 From: Takametaka Date: Thu, 2 Jul 2020 15:34:59 +0200 Subject: [PATCH 2/2] New version of agda.ml that doesn't work (yet) --- src/sttfa/export/agda.ml | 56 +++++++++++++++++++--------------------- 1 file changed, 26 insertions(+), 30 deletions(-) diff --git a/src/sttfa/export/agda.ml b/src/sttfa/export/agda.ml index 089acd5..545492b 100644 --- a/src/sttfa/export/agda.ml +++ b/src/sttfa/export/agda.ml @@ -13,9 +13,6 @@ let forbidden_id = ref ["abstract";"consructor";"data";"do";"eta-equality";"fiel "record";"renaming";"rexrite";"Set";"syntax";"tactic";"unquote";"unquoteDecl"; "unquoteDef";"using";"variable";"where";"with"] -(* when _ used as wildcard, leave it - otherwise, change it to :: (- is forbidden because it may lead to inline comments) - because i would be interpreted as mix-fix operator *) let sanitize id = if id = "_" then id @@ -36,14 +33,10 @@ let rec print_list sep pp oc = function | x::t -> Format.fprintf oc "(%a)%s%a" pp x sep (print_list sep pp) t let print_dep oc dep = - (* let dep = sanitize dep in *) Format.fprintf oc "open import %s\n" dep let print_name oc (md,id) = let id = sanitize id in - (* let md = sanitize md in *) - (* sanitize md causes problems, one might need to rename all files with : - (cd export/agda ; rename _ :: *.agda) *) if !cur_md = md then Format.fprintf oc "%s" id else @@ -64,7 +57,7 @@ let rec print__ty oc = function Format.fprintf oc "%a" print_name tyOp | TyOp(tyOp, _tys) -> Format.fprintf oc "%a %a" print_name tyOp (print_list " " print__ty) _tys - | Prop -> Format.fprintf oc "Prop" + | Prop -> Format.fprintf oc "Set" and print__ty_wp fmt _ty = match _ty with @@ -75,8 +68,7 @@ and print__ty_wp fmt _ty = let rec print_ty oc = function | ForallK(var, ty) -> - (* Format.fprintf oc "forall (%a : Set) -> %a" print_var var print_ty ty *) - Format.fprintf oc "(%a : Set) -> %a" print_var var print_ty ty + Format.fprintf oc "{^k : Level} -> forall (%a : Set ^k) -> %a" print_var var print_ty ty | Ty(_ty) -> print__ty oc _ty let rec print__te oc = function @@ -84,17 +76,16 @@ let rec print__te oc = function Format.fprintf oc "%a" print_var var | Abs(var,_ty,_te) -> Format.fprintf oc "\\(%a : %a) -> %a" print_var var print__ty_wp _ty print__te _te - | App(Abs _ as _tel,_ter) -> (* Some proofs are not in beta normal form (is it true for Agda ?) *) - Format.fprintf oc "((%a) %a)" print__te _tel print__te_wp _ter (* not sure *) + | App(Abs _ as _tel,_ter) -> + Format.fprintf oc "((%a) %a)" print__te _tel print__te_wp _ter | App(_tel,_ter) -> - Format.fprintf oc "%a %a" print__te _tel print__te_wp _ter (* not sure *) + Format.fprintf oc "%a %a" print__te _tel print__te_wp _ter | Forall(var,_ty,_te) -> - Format.fprintf oc "(%a : %a) -> %a" print_var var print__ty_wp _ty print__te _te - (* Format.fprintf oc "forall (%a : %a) -> %a" print_var var print__ty_wp _ty print__te _te *) + Format.fprintf oc "forall (%a : %a) -> %a" print_var var print__ty_wp _ty print__te _te | Impl(_tel,_ter) -> Format.fprintf oc "%a -> %a" print__te_wp _tel print__te _ter | AbsTy(var, _te) -> - Format.fprintf oc "\\(%a : Set) -> %a" print_var var print__te _te (* ie id = \(A : Set) -> \(x : A) -> x *) + Format.fprintf oc "\\(%a : Set ^k) -> %a" print_var var print__te _te | Cst(cst, []) -> Format.fprintf oc "%a" print_name cst | Cst(cst, _tys) -> @@ -107,9 +98,8 @@ and print__te_wp fmt _te = | _ -> Format.fprintf fmt "(%a)" print__te _te let rec print_te oc = function - | ForallP(var,te) -> - Format.fprintf oc "(%a : _) -> %a" print_var var print_te te - (* Format.fprintf oc "forall %a -> %a" print_var var print_te te *) + | ForallP(var,te) -> (* Can actually be followed by other ForallP *) + Format.fprintf oc "{^p : Level} -> forall (%a : Set ^p) -> %a" print_var var print_te te | Te(_te) -> print__te oc _te let rec print_proof oc = function @@ -117,7 +107,7 @@ let rec print_proof oc = function | Lemma(name,_) -> Format.fprintf oc "%a" print_name name | Conv(_,proof,_) -> Format.fprintf oc "%a" print_proof proof | ImplE(_,left,right) -> Format.fprintf oc "(%a) (%a)" print_proof left print_proof right - | ImplI(_,proof,var) -> (* abstraction to indtroduce Impl, needs to extract term from judgment *) + | ImplI(_,proof,var) -> let j' = judgment_of proof in let _,_te = TeSet.choose (TeSet.filter (fun (x,_) -> if x = var then true else false) j'.hyp) in Format.fprintf oc "\\(%a : %a) -> (%a)" print_var var print__te _te print_proof proof @@ -128,32 +118,37 @@ let rec print_proof oc = function Format.fprintf oc "\\(%a : %a) -> %a" print_var var print__ty _ty print_proof proof | ForallPE(_,proof,_ty) -> Format.fprintf oc "(%a) (%a)" print_proof proof print__ty _ty | ForallPI(_,proof,var) -> - Format.fprintf oc "\\(%a : Set) -> %a" print_var var print_proof proof + Format.fprintf oc "\\(%a : Set ^p) -> %a" print_var var print_proof proof let print_item oc = function | Parameter(name,ty) -> - Format.fprintf oc "%a : %a@." print_name name print_ty ty - | Definition(name,ty,te) -> - Format.fprintf oc "%a : %a@.%a = %a@.@." print_name name print_ty ty print_name name print_te te + Format.fprintf oc "postulate %a : %a@." print_name name print_ty ty + | Definition(name,ForallK(_,_),te) -> + Format.fprintf oc "%a : {^k : Level} -> _@.%a {^k} = %a@.@." print_name name print_name name print_te te + | Definition(name,_,te) -> + Format.fprintf oc "%a : _@.%a = %a@.@." print_name name print_name name print_te te | Axiom (name,te) -> Format.fprintf oc "postulate %a : %a@." print_name name print_te te - | Theorem(name,te,proof) -> - Format.fprintf oc "%a : %a@.%a = %a@.@." print_name name print_te te print_name name print_proof proof + | Theorem(name,ForallP(_,_),proof) -> + Format.fprintf oc "%a : {^p : Level} -> _@.%a {^p} = %a@.@." print_name name print_name name print_proof proof + | Theorem(name,_,proof) -> + Format.fprintf oc "%a : _@.%a = %a@.@." print_name name print_name name print_proof proof | TypeDecl(tyop,arity) -> Format.fprintf oc "%a : %a@." print_name tyop print_arity arity | TypeDef (name,_,_) -> Format.fprintf oc "-- Type definition (for %a) not handled right now@." print_name name +(* Agda.Primitive needed for Level *) let print_ast : Format.formatter -> ?mdeps:Ast.mdeps -> Ast.ast -> unit = fun fmt ?mdeps:_ ast -> cur_md := ast.md; - Format.fprintf fmt "module %s where\n" !cur_md; + Format.fprintf fmt "module %s where\nopen import Agda.Primitive\n" !cur_md; D.QSet.iter (print_dep fmt) ast.dep; List.iter (print_item fmt) ast.items -(* not used ? +(* let print_meta_ast fmt meta_ast = let print_ast fmt ast = - Format.fprintf fmt "module %s where\n" ast.md; (* I don't think you need to indent for a top-level module *) + Format.fprintf fmt "module %s where\n" ast.md; (* You need to indent for a top-level module *) print_ast fmt ast; in List.iter (print_ast fmt) meta_ast @@ -161,9 +156,10 @@ let print_meta_ast fmt meta_ast = let to_string fmt = Format.asprintf "%a" fmt *) +(* TODO : update it according to print_item *) let string_of_item = function | Parameter((_,id),ty) -> - Format.asprintf "%s : %a" id print_ty ty + Format.asprintf "postulate %s : %a" id print_ty ty | Definition((_,id),ty,te) -> Format.asprintf "%s : %a@.%s = %a" id print_ty ty id print_te te | Axiom((_,id),te) ->